nLab interval category

Redirected from "interval proset".

Contents

Definition

Interval category

The interval category – often denoted 2\mathbf{2} or II or Δ[1]\Delta[1] – is the category with two objects and precisely one nontrivial morphism connecting them:

I={01}. I = \left\{ 0 \to 1 \right\} \,.

It is also commonly called the interval preorder or the interval poset (since it is indeed a poset).

The interval category serves as a combinatorial model for the directed interval. It is the directed canonical interval object in Cat. It is also called the walking arrow. It might also be called the “arrow category” although that term is also used for a category of functors out of 2\mathbf{2}.

The notation 2\mathbf{2} comes from the fact that the interval category is also the ordinal number 22 regarded as a poset, regarded as a category.

It also appears as

Since every category is also an (n,r)-category for n,r1n,r \geq 1, we may regard II also as some (n,r)(n,r)-category. For instance regarded as a (∞,1)-category and modeled as a quasi-category, the interval category is the simplicial set Δ[1]\Delta[1].

 In (homotopy) type theory

In type theory, the type of objects of the interval category is the booleans type 𝟚\mathbb{2}. The relation on it 𝟚\leq_\mathbb{2} can be inductively generated by

  • a term p:0 𝟚1p:0 \leq_\mathbb{2} 1

  • a term refl 0:0 𝟚0\mathrm{refl}_0:0 \leq_\mathbb{2} 0

  • a term refl 1:1 𝟚1\mathrm{refl}_1:1 \leq_\mathbb{2} 1

It can equivalently be defined recursively on 𝟚\mathbb{2} by

  • (0 𝟚0)(0 \leq_\mathbb{2} 0) \equiv \top
  • (0 𝟚1)(0 \leq_\mathbb{2} 1) \equiv \top
  • (1 𝟚0)(1 \leq_\mathbb{2} 0) \equiv \bot
  • (1 𝟚1)(1 \leq_\mathbb{2} 1) \equiv \top

Since the symbol 𝕀\mathbb{I} is sometimes used for the interval type in homotopy type theory, which is contractible, it may be better to avoid it for the interval category unless the meaning is clear from context.

Interval groupoid

Inverting the single non-identity arrow of the interval category, we obtain the interval groupoid, which is an (undirected) interval object in Cat and Grpd.

Applications

The interval category is one of those diagram category that are not terribly interesting in themselves, but that serve an important role in category theory as a whole.

For instance a natural transformation η:FG\eta : F \Rightarrow G between two functors F,G:CDF,G : C \to D is precisely the same as a strictly commuting diagram

C×{0} F C×I η D G C×{1} \array{ C \times \{0\} \\ \downarrow & \searrow^{\mathrlap{F}} \\ C \times I &\stackrel{\eta}{\to}& D \\ \uparrow & \nearrow_{\mathrlap{G}} \\ C \times \{1\} }

in Cat, where on the left we have the cartesian product of CC with II.

Accordingly, for I isoI_{iso} the interval groupoid, a natural isomorphism η:FG\eta : F \Rightarrow G is the same as a diagram

C×{0} F C×I iso η D G C×{1}. \array{ C \times \{0\} \\ \downarrow & \searrow^{\mathrlap{F}} \\ C \times I_{iso} &\stackrel{\eta}{\to}& D \\ \uparrow & \nearrow_{\mathrlap{G}} \\ C \times \{1\} } \,.

This is a left homotopy in CatCat.

Dually, forming the functor category

Arr(D):=[I,D] Arr(D) := [I,D]

from the interval category produces the arrow category of DD, and a natural transformation η\eta is also the same as a diagram

D×{0} F C η [I,D] G D×{1}. \array{ && D \times \{0\} \\ & {}^{\mathllap{F}}\nearrow & \uparrow \\ C &\stackrel{\eta}{\to}& [I,D] \\ & {}_{\mathllap{G}}\searrow & \downarrow \\ && D \times \{1\} } \,.

With II replaced by I isoI_{iso} this is again a natural isomorphism, now represented as a right homotopy in Cat.

The analogous statements are true in higher category theory.

Last revised on August 23, 2023 at 02:13:54. See the history of this page for a list of all contributions to it.